<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>GMFFManager</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="GMFFManager";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/GMFFInputFile.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/GMFFMandatoryModelNotFoundException.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/GMFFManager.html" target="_top">Frames</a></li>
<li><a href="GMFFManager.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.gmff</div>
<h2 title="Class GMFFManager" class="title">Class GMFFManager</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.gmff.GMFFManager</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">GMFFManager</span>
extends java.lang.Object</pre>
<div class="block">Serves as a central data store for GMFF work in progress and as the primary
 interface for access to GMFF services.
 <p>
 One thing that is different about <code>GMFFManager</code> than other "manager"
 type classes in mmj2 is that the <code>GMFFManager</code> object is instantiated
 by the <code>LogicalSystemBoss</code> in the <code>util</code> package rather than the
 <code>GMFFBoss</code>. This is because Metamath $t Comment statement(s) are
 accumulated during the <code>LoadFile</code> process -- though not parsed at that
 time. Hence, a reference to the <code>GMFFManager</code> instance is stored in
 <code>LogicalSystem</code>.
 <p>
 Another thing that is different than typical mmj2 processing is that the GMFF
 RunParms which establish settings for parameters are not validated when the
 RunParms are initially read. Nothing in GMFF happens until the first time the
 user -- or a command-style GMFF RunParm -- requests that GMFF typeset
 something. This functionality matches the way Metamath works and also saves
 users who have no interest in using GMFF from aggravation if there are errors
 in the GMFF-related inputs. A side-effect of delayed validation of GMFF
 RunParms is additional complexity. <code>GMFFManager</code> deals with that
 complexity in <code>initialization()</code> where all of the cached RunParms are
 validated and merged with default settings for parameters.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/gmff/GMFFManager.html#GMFFManager(java.io.File, mmj.lang.Messages)">GMFFManager</a></strong>(java.io.File&nbsp;filePath,
           <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Standard constructor.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#accumInputGMFFExportParms(mmj.gmff.GMFFExportParms)">accumInputGMFFExportParms</a></strong>(<a href="../../mmj/gmff/GMFFExportParms.html" title="class in mmj.gmff">GMFFExportParms</a>&nbsp;inputGMFFExportParms)</code>
<div class="block">Caches parameters from one RunParm for later validation and use.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#accumInputGMFFUserTextEscapesList(mmj.gmff.GMFFUserTextEscapes)">accumInputGMFFUserTextEscapesList</a></strong>(<a href="../../mmj/gmff/GMFFUserTextEscapes.html" title="class in mmj.gmff">GMFFUserTextEscapes</a>&nbsp;inputGMFFUserTextEscapes)</code>
<div class="block">Caches parameters from one RunParm for later validation and use.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#cacheTypesettingCommentForGMFF(java.lang.String)">cacheTypesettingCommentForGMFF</a></strong>(java.lang.String&nbsp;comment)</code>
<div class="block">Caches one Metamath $t Comment statement for later validation and use.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#exportFromFolder(java.lang.String, java.lang.String, java.lang.String, java.lang.String, java.lang.String)">exportFromFolder</a></strong>(java.lang.String&nbsp;inputDirectory,
                java.lang.String&nbsp;theoremLabelOrAsterisk,
                java.lang.String&nbsp;inputFileType,
                java.lang.String&nbsp;maxNumberToExport,
                java.lang.String&nbsp;appendFileNameIn)</code>
<div class="block">Exports one or a range of Proof Worksheets of a given file type from a
 designated directory.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#exportProofWorksheet(java.lang.String, java.lang.String)">exportProofWorksheet</a></strong>(java.lang.String&nbsp;proofText,
                    java.lang.String&nbsp;appendFileName)</code>
<div class="block">Exports a single Proof Worksheet to files in the requested formats.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#exportTheorem(java.lang.String, java.lang.String, java.lang.String, mmj.pa.ProofAsst)">exportTheorem</a></strong>(java.lang.String&nbsp;theoremLabelOrAsterisk,
             java.lang.String&nbsp;maxNumberToExport,
             java.lang.String&nbsp;appendFileNameIn,
             <a href="../../mmj/pa/ProofAsst.html" title="class in mmj.pa">ProofAsst</a>&nbsp;proofAsst)</code>
<div class="block">Exports one theorem or a range of theorems from <code>LogicalSystem</code>.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#forceReinitialization()">forceReinitialization</a></strong>()</code>
<div class="block">Forces GMFF to re-initialize itself the next time a service request is
 received by settting <code>gmffInitialized</code> to <code>false</code>.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#generateInitializationAuditReport()">generateInitializationAuditReport</a></strong>()</code>
<div class="block">Generates and outputs to the Messages object an audit report of the final
 results of GMFF initialization showing the parameters and settings in
 use.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#generateTypesettingDefinitionsReport()">generateTypesettingDefinitionsReport</a></strong>()</code>
<div class="block">Generates and outputs to the Messages object an audit report of the
 Metamath $t typesetting definitions after parsing of the input Metamath
 file.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#getMessages()">getMessages</a></strong>()</code>
<div class="block">Gets the <code>messages</code> object.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#getSymTbl()">getSymTbl</a></strong>()</code>
<div class="block">Gets the <code>symTbl</code> for use in generating GMFF exports.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#gmffExportOneTheorem(java.lang.String, java.lang.String, mmj.pa.ProofAsst)">gmffExportOneTheorem</a></strong>(java.lang.String&nbsp;theoremLabel,
                    java.lang.String&nbsp;appendFileName,
                    <a href="../../mmj/pa/ProofAsst.html" title="class in mmj.pa">ProofAsst</a>&nbsp;proofAsst)</code>
<div class="block">Exports one <code>Theorem</code> from the <code>LogicalSystem</code>.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#gmffExportOneTheorem(mmj.lang.Theorem, java.lang.String, mmj.pa.ProofAsst)">gmffExportOneTheorem</a></strong>(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem,
                    java.lang.String&nbsp;appendFileName,
                    <a href="../../mmj/pa/ProofAsst.html" title="class in mmj.pa">ProofAsst</a>&nbsp;proofAsst)</code>
<div class="block">Exports one <code>Theorem</code> from the <code>LogicalSystem</code>.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#gmffInitialize(boolean)">gmffInitialize</a></strong>(boolean&nbsp;printTypesettingDefinitions)</code>
<div class="block">Calls <code>initialize()</code>, generates an audit report of GMFF RunParms
 and default settings,mand if requested, prints the typesetting
 definitions obtained from the input Metamath file(s) $t Comment
 statements.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#isGMFFInitialized()">isGMFFInitialized</a></strong>()</code>
<div class="block">Returns the <code>gmffInitialized</code> boolean variable.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#parseMetamathTypesetComment(java.lang.String, java.lang.String, java.lang.String, boolean)">parseMetamathTypesetComment</a></strong>(java.lang.String&nbsp;typesetDefKeyword,
                           java.lang.String&nbsp;myDirectory,
                           java.lang.String&nbsp;myMetamathTypesetCommentFileName,
                           boolean&nbsp;runParmPrintOption)</code>
<div class="block">Implements RunParm GMFFParseMMTypesetDefsComment.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#setInputGMFFUserExportChoice(mmj.gmff.GMFFUserExportChoice)">setInputGMFFUserExportChoice</a></strong>(<a href="../../mmj/gmff/GMFFUserExportChoice.html" title="class in mmj.gmff">GMFFUserExportChoice</a>&nbsp;choice)</code>
<div class="block">Stores the contents of the <code>GMFFUserExportChoice</code> from one RunParm
 for later validation and use.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/GMFFManager.html#setSymTbl(java.util.Map)">setSymTbl</a></strong>(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl)</code>
<div class="block">Sets the <code>symTbl</code> for use in generating GMFF exports.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="GMFFManager(java.io.File, mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>GMFFManager</h4>
<pre>public&nbsp;GMFFManager(java.io.File&nbsp;filePath,
           <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</pre>
<div class="block">Standard constructor.
 <p>
 Called by <code>LogicalSystemBoss</code> when the first <code>LoadFile</code>
 RunParm is executed.
 <p>
 Sets up GMFF data structures but does not load them. Sets
 <code>gmffInitialized</code> to <code>false</code> to trigger initialization when
 the first GMFF service request is received.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>filePath</code> - path for building directories.</dd><dd><code>messages</code> - The Messages object.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="gmffInitialize(boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>gmffInitialize</h4>
<pre>public&nbsp;void&nbsp;gmffInitialize(boolean&nbsp;printTypesettingDefinitions)
                    throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Calls <code>initialize()</code>, generates an audit report of GMFF RunParms
 and default settings,mand if requested, prints the typesetting
 definitions obtained from the input Metamath file(s) $t Comment
 statements.
 <p>
 This function is called by GMFFBoss in response to a
 <code>GMFFInitialize</code> RunParm.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>printTypesettingDefinitions</code> - prints data from Metamath $t Comments
            for which there are <code>GMFFExportParms</code> with matching
            <code>typesetDefs</code> (we don't load data from the $t's unless
            it is needed.)</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if an error occurred</dd></dl>
</li>
</ul>
<a name="accumInputGMFFExportParms(mmj.gmff.GMFFExportParms)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>accumInputGMFFExportParms</h4>
<pre>public&nbsp;void&nbsp;accumInputGMFFExportParms(<a href="../../mmj/gmff/GMFFExportParms.html" title="class in mmj.gmff">GMFFExportParms</a>&nbsp;inputGMFFExportParms)</pre>
<div class="block">Caches parameters from one RunParm for later validation and use.
 <p>
 Also invokes <code>forceReinitialization()</code> which sets
 <code>gmffInitialized = false</code> to force re-initialization of GMFF the
 next time a service request is made.
 <p>
 This function is called by <code>GMFFBoss</code> in response to a
 <code>GMFFExportParms</code> RunParm.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>inputGMFFExportParms</code> - data from GMFFExportParms RunParm.</dd></dl>
</li>
</ul>
<a name="accumInputGMFFUserTextEscapesList(mmj.gmff.GMFFUserTextEscapes)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>accumInputGMFFUserTextEscapesList</h4>
<pre>public&nbsp;void&nbsp;accumInputGMFFUserTextEscapesList(<a href="../../mmj/gmff/GMFFUserTextEscapes.html" title="class in mmj.gmff">GMFFUserTextEscapes</a>&nbsp;inputGMFFUserTextEscapes)</pre>
<div class="block">Caches parameters from one RunParm for later validation and use.
 <p>
 Also invokes <code>forceReinitialization()</code> which sets
 <code>gmffInitialized = false</code> to force re-initialization of GMFF the
 next time a service request is made.
 <p>
 This function is called by <code>GMFFBoss</code> in response to a
 <code>GMFFUserTextEscapes</code> RunParm.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>inputGMFFUserTextEscapes</code> - data from GMFFUserTextEscapes RunParm.</dd></dl>
</li>
</ul>
<a name="cacheTypesettingCommentForGMFF(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>cacheTypesettingCommentForGMFF</h4>
<pre>public&nbsp;void&nbsp;cacheTypesettingCommentForGMFF(java.lang.String&nbsp;comment)</pre>
<div class="block">Caches one Metamath $t Comment statement for later validation and use.
 <p>
 Also invokes <code>forceReinitialization()</code> which sets
 <code>gmffInitialized = false</code> to force re-initialization of GMFF the
 next time a service request is made.
 <p>
 This function is called by <code>LogicalSystem</code> during processing of a
 <code>LoadFile</code> RunParm.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>comment</code> - String Metamath $t Comment statement as stored in
            <code>SrcStmt</code> (the "$(" and "$)" delimiters are removed at
            this pointand the first token is "$t").</dd></dl>
</li>
</ul>
<a name="setInputGMFFUserExportChoice(mmj.gmff.GMFFUserExportChoice)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setInputGMFFUserExportChoice</h4>
<pre>public&nbsp;void&nbsp;setInputGMFFUserExportChoice(<a href="../../mmj/gmff/GMFFUserExportChoice.html" title="class in mmj.gmff">GMFFUserExportChoice</a>&nbsp;choice)</pre>
<div class="block">Stores the contents of the <code>GMFFUserExportChoice</code> from one RunParm
 for later validation and use.
 <p>
 Also invokes <code>forceReinitialization()</code> which sets
 <code>gmffInitialized = false</code> to force re-initialization of GMFF the
 next time a service request is made.
 <p>
 This function is called by <code>GMFFBoss</code> in response to a
 <code>GMFFUserExportChoice</code> RunParm.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>choice</code> - from GMFFUserExportChoice RunParm.</dd></dl>
</li>
</ul>
<a name="setSymTbl(java.util.Map)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setSymTbl</h4>
<pre>public&nbsp;void&nbsp;setSymTbl(java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl)</pre>
<div class="block">Sets the <code>symTbl</code> for use in generating GMFF exports.
 <p>
 This function is called by the <code>LogicalSystem</code> constructor -- which
 itself is excuted during processing of the first <code>LoadFile</code>
 RunParm. <code>symTbl</code> is itself constructed during construction of
 <code>LogicalSystem</code> so this function is necessary even though
 <code>GMFFManager</code> is passed as an argument to the <code>LogicalSystem</code>
 constructor (a somewhat circular arrangement.)
 <p>
 <code>symTbl</code> is needed because an error message is generated when a
 symbol to be typeset is not found in the Metamath $t definitions, but
 only if the symbol string is really a valid symbol (and is not a
 <code>WorkVar</code>.) (GMFF not not require that Proof Worksheets be valid,
 just that the Proof Worksheet format is loosely followed.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>symTbl</code> - The Symbol Table Map from <code>LogicalSystem</code></dd></dl>
</li>
</ul>
<a name="getSymTbl()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSymTbl</h4>
<pre>public&nbsp;java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;getSymTbl()</pre>
<div class="block">Gets the <code>symTbl</code> for use in generating GMFF exports.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>The Symbol Table Map, <code>symTbl</code> from <code>LogicalSystem</code></dd></dl>
</li>
</ul>
<a name="getMessages()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMessages</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;getMessages()</pre>
<div class="block">Gets the <code>messages</code> object.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>The Messages object used to store error and informational
         messages during mmj2 processing.</dd></dl>
</li>
</ul>
<a name="isGMFFInitialized()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isGMFFInitialized</h4>
<pre>public&nbsp;boolean&nbsp;isGMFFInitialized()</pre>
<div class="block">Returns the <code>gmffInitialized</code> boolean variable.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>true if GMFF already initialized, otherwise false.</dd></dl>
</li>
</ul>
<a name="forceReinitialization()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>forceReinitialization</h4>
<pre>public&nbsp;void&nbsp;forceReinitialization()</pre>
<div class="block">Forces GMFF to re-initialize itself the next time a service request is
 received by settting <code>gmffInitialized</code> to <code>false</code>.</div>
</li>
</ul>
<a name="exportFromFolder(java.lang.String, java.lang.String, java.lang.String, java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exportFromFolder</h4>
<pre>public&nbsp;void&nbsp;exportFromFolder(java.lang.String&nbsp;inputDirectory,
                    java.lang.String&nbsp;theoremLabelOrAsterisk,
                    java.lang.String&nbsp;inputFileType,
                    java.lang.String&nbsp;maxNumberToExport,
                    java.lang.String&nbsp;appendFileNameIn)
                      throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Exports one or a range of Proof Worksheets of a given file type from a
 designated directory.
 <p>
 This function implements the <code>GMFFExportFromFolder</code> RunParm
 command.
 <p>
 The sort sequence used to select and output Proof Worksheets is File Name
 minus File Type.
 <p>
 Refer to mmj2\doc\gmffdoc\C:\mmj2jar\GMFFDoc\GMFFRunParms.txt for more
 info about the parameters on the <code>GMFFExportFromFolder</code> RunParm.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>inputDirectory</code> - The Directory to export Proof Worksheets from</dd><dd><code>theoremLabelOrAsterisk</code> - Either a theorem label or "*". If theorem
            label input then that is used as the starting point, otherwise
            processing begins at the first file in the directory.</dd><dd><code>inputFileType</code> - File Type to select, including the "." (e.g. ".mmp")</dd><dd><code>maxNumberToExport</code> - Limits the number of exports processed. Must be
            greater than zero and less then 2 billionish...</dd><dd><code>appendFileNameIn</code> - Specifies an append-mode file name to which all
            of the exported proofs will be written -- within the folder
            specified for each Export Type on the GMFFExportParms RunParm;
            overrides the normal name assigned to an export file.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - is errors encountered.</dd></dl>
</li>
</ul>
<a name="exportTheorem(java.lang.String, java.lang.String, java.lang.String, mmj.pa.ProofAsst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exportTheorem</h4>
<pre>public&nbsp;void&nbsp;exportTheorem(java.lang.String&nbsp;theoremLabelOrAsterisk,
                 java.lang.String&nbsp;maxNumberToExport,
                 java.lang.String&nbsp;appendFileNameIn,
                 <a href="../../mmj/pa/ProofAsst.html" title="class in mmj.pa">ProofAsst</a>&nbsp;proofAsst)
                   throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Exports one theorem or a range of theorems from <code>LogicalSystem</code>.
 <p>
 This function implements the <code>GMFFExportTheorem</code> RunParm command.
 <p>
 The sort sequence used to select and output thereoms is <code>MObj.seq</code>
 -- that is, order of appearance in the <code>LogicalSystem</code>.
 <p>
 Refer to mmj2\doc\gmffdoc\C:\mmj2jar\GMFFDoc\GMFFRunParms.txt for more
 info about the parameters on the <code>GMFFExportThereom</code> RunParm.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>theoremLabelOrAsterisk</code> - Either a theorem label or "*". If theorem
            label input then that is used as the starting point, otherwise
            processing begins at the first file in the directory.</dd><dd><code>maxNumberToExport</code> - Limits the number of exports processed. Must be
            greater than zero and less then 2 billionish...</dd><dd><code>appendFileNameIn</code> - Specifies an append-mode file name to which all
            of the exported proofs will be written -- within the folder
            specified for each Export Type on the GMFFExportParms RunParm;
            overrides the normal name assigned to an export file.</dd><dd><code>proofAsst</code> - The <code>ProofAsst</code> object, used to format Proof
            Worksheets from Metamath (RPN) proofs.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - is errors encountered.</dd></dl>
</li>
</ul>
<a name="gmffExportOneTheorem(mmj.lang.Theorem, java.lang.String, mmj.pa.ProofAsst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>gmffExportOneTheorem</h4>
<pre>public&nbsp;void&nbsp;gmffExportOneTheorem(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem,
                        java.lang.String&nbsp;appendFileName,
                        <a href="../../mmj/pa/ProofAsst.html" title="class in mmj.pa">ProofAsst</a>&nbsp;proofAsst)
                          throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Exports one <code>Theorem</code> from the <code>LogicalSystem</code>. loaded
 <p>
 This function is called by other functions in <code>GMFFManager</code> but it
 would be perfectly valid to call it externally.
 <p>
 This function calls <code>ProofAsst.exportOneTheorem</code> which creates a
 Proof Worksheet from a Metamath (RPN) proof. If the theorem's proof is
 incomplete or invalid, or if it contains no assertions, an error message
 results (and if input argument <code>theorem</code> is null an
 <code>IllegalArgumentException</code> will result ;-)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>theorem</code> - <code>Theorem</code> to be exported.</dd><dd><code>appendFileName</code> - Specifies an append-mode file name to which
            exported proof will be written -- within the folder specified
            for each Export Type on the GMFFExportParms RunParm; overrides
            the normal name assigned to an export file.</dd><dd><code>proofAsst</code> - The <code>ProofAsst</code> object, used to format Proof
            Worksheets from Metamath (RPN) proofs.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - is errors encountered.</dd></dl>
</li>
</ul>
<a name="gmffExportOneTheorem(java.lang.String, java.lang.String, mmj.pa.ProofAsst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>gmffExportOneTheorem</h4>
<pre>public&nbsp;void&nbsp;gmffExportOneTheorem(java.lang.String&nbsp;theoremLabel,
                        java.lang.String&nbsp;appendFileName,
                        <a href="../../mmj/pa/ProofAsst.html" title="class in mmj.pa">ProofAsst</a>&nbsp;proofAsst)
                          throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Exports one <code>Theorem</code> from the <code>LogicalSystem</code>. loaded
 <p>
 This function is called by other functions in <code>GMFFManager</code> but it
 would be perfectly valid to call it externally.
 <p>
 This function calls <code>ProofAsst.exportOneTheorem</code> which creates a
 Proof Worksheet from a Metamath (RPN) proof. If the theorem's proof is
 incomplete or invalid, or if it contains no assertions, an error message
 results -- and if input argument <code>theoremLabel</code> is null or invalid
 an exception is thrown...</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>theoremLabel</code> - label of <code>Theorem</code> to be exported.</dd><dd><code>appendFileName</code> - Specifies an append-mode file name to which
            exported proof will be written -- within the folder specified
            for each Export Type on the GMFFExportParms RunParm; overrides
            the normal name assigned to an export file.</dd><dd><code>proofAsst</code> - The <code>ProofAsst</code> object, used to format Proof
            Worksheets from Metamath (RPN) proofs.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - is errors encountered.</dd></dl>
</li>
</ul>
<a name="exportProofWorksheet(java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exportProofWorksheet</h4>
<pre>public&nbsp;java.lang.String&nbsp;exportProofWorksheet(java.lang.String&nbsp;proofText,
                                    java.lang.String&nbsp;appendFileName)
                                      throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Exports a single Proof Worksheet to files in the requested formats.
 <p>
 This function is called by <code>ProofAsst</code> and by various functions in
 <code>GMFFManager</code>.
 <p>
 The following functions are performed:
 <p>
 <ol>
 <li>Initializes GMFF if necessary.
 <li>Throws an exception if the parameter settings do not include at least
 one active export format.
 <li>Loads the input proofText into a new <code>ProofWorksheetCache</code>
 object
 <li>invokes each active export request passing the
 <code>ProofWorksheetCache</code> and accumulating confirmation messages from
 them in return.
 <li>returns the accumulated confirmation messages to the caller.
 </ol></div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofText</code> - String containing text in the format of an mmj2 Proof
            Worksheet.</dd><dd><code>appendFileName</code> - name of a file to which export data should be
            appended (in the proper directory for the Export Type), or
            <code>null</code> if GMFF is supposed to generate the name.</dd>
<dt><span class="strong">Returns:</span></dt><dd>String containing confirmation messages about successful
         export(s) if no errors occurred.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if error found.</dd></dl>
</li>
</ul>
<a name="parseMetamathTypesetComment(java.lang.String, java.lang.String, java.lang.String, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>parseMetamathTypesetComment</h4>
<pre>public&nbsp;void&nbsp;parseMetamathTypesetComment(java.lang.String&nbsp;typesetDefKeyword,
                               java.lang.String&nbsp;myDirectory,
                               java.lang.String&nbsp;myMetamathTypesetCommentFileName,
                               boolean&nbsp;runParmPrintOption)
                                 throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Implements RunParm GMFFParseMMTypesetDefsComment.
 <p>
 This function is primarily used for testing. It parses a file containing
 a single Metamath comment statement -- of the $t variety. Because it is
 intended for standalone use in testing, it does not require GMFF
 initialization prior to use, and it does not check for or trigger GMFF
 initialization.
 <p>
 The code is quick and dirty because it is just used for testing.
 Efficiency not an issue.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>typesetDefKeyword</code> - The Metamath $t keyword to select for parsing
            (e.g. "htmldef")</dd><dd><code>myDirectory</code> - The directory containing the Metamath .mm file to
            parse.</dd><dd><code>myMetamathTypesetCommentFileName</code> - File Name in myDirectory to
            parse.</dd><dd><code>runParmPrintOption</code> - if true prints the input, including the
            directory, file name, typesetDefKeyword and the entire
            Metamath file.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if errors found.</dd></dl>
</li>
</ul>
<a name="generateInitializationAuditReport()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>generateInitializationAuditReport</h4>
<pre>public&nbsp;void&nbsp;generateInitializationAuditReport()</pre>
<div class="block">Generates and outputs to the Messages object an audit report of the final
 results of GMFF initialization showing the parameters and settings in
 use.</div>
</li>
</ul>
<a name="generateTypesettingDefinitionsReport()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>generateTypesettingDefinitionsReport</h4>
<pre>public&nbsp;void&nbsp;generateTypesettingDefinitionsReport()</pre>
<div class="block">Generates and outputs to the Messages object an audit report of the
 Metamath $t typesetting definitions after parsing of the input Metamath
 file.</div>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/GMFFInputFile.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/GMFFMandatoryModelNotFoundException.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/GMFFManager.html" target="_top">Frames</a></li>
<li><a href="GMFFManager.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
